\begin{tabbing}
config{-}antecedent(${\it es}$;${\it Master}$;${\it Config}$;$c$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$e$:E(${\it Config}$). ($c$($e$) $<$ $e$))\+
\\[0ex]\& ($\forall$$e_{1}$, $e_{2}$:E(${\it Config}$). ($c$($e_{1}$) $<$ $c$($e_{2}$)) $\Rightarrow$ (loc($e_{1}$) = loc($e_{2}$)) $\Rightarrow$ ($e_{1}$ $<$loc $e_{2}$))
\\[0ex]\& (\=$\forall$$e$:E(${\it Config}$).\+
\\[0ex]let \=$m$\= = ${\it Master}$($c$($e$)) in\+\+
\\[0ex]chain\_config\_ind(${\it Config}$($e$);($\uparrow$cmconfig?($m$))
\-\\[0ex]\& ($\parallel$cmconfig{-}list($m$)$\parallel$ $\geq$ 1 )
\\[0ex]\& loc($e$) = hd(cmconfig{-}list($m$));($\uparrow$cmconfig?($m$))
\\[0ex]\& ($\neg$($\uparrow$null(cmconfig{-}list($m$))))
\\[0ex]\& loc($e$) = last(cmconfig{-}list($m$));$i$.($\uparrow$cmconfig?($m$))
\\[0ex]\& ($\exists$\=${\it index}$:\{0..$\parallel$cmconfig{-}list($m$)$\parallel^{-}$\}\+
\\[0ex]((0 $<$ ${\it index}$)
\\[0ex]\& loc($e$) = cmconfig{-}list($m$)[${\it index}$]
\\[0ex]\& $i$ = cmconfig{-}list($m$)[(${\it index}$ {-} 1)]));$i$,$n$.($\uparrow$cmseq?($m$))
\-\\[0ex]\& $i$ = cmseq{-}to($m$)
\\[0ex]\& loc($e$) = cmseq{-}from($m$)
\\[0ex]\& $n$ = cmseq{-}num($m$)))
\-\-\-
\end{tabbing}